Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    2nd(cons1(X,cons(Y,Z)))  → Y
2:    2nd(cons(X,X1))  → 2nd(cons1(X,activate(X1)))
3:    from(X)  → cons(X,n__from(n__s(X)))
4:    from(X)  → n__from(X)
5:    s(X)  → n__s(X)
6:    activate(n__from(X))  → from(activate(X))
7:    activate(n__s(X))  → s(activate(X))
8:    activate(X)  → X
There are 6 dependency pairs:
9:    2nd#(cons(X,X1))  → 2nd#(cons1(X,activate(X1)))
10:    2nd#(cons(X,X1))  → ACTIVATE(X1)
11:    ACTIVATE(n__from(X))  → FROM(activate(X))
12:    ACTIVATE(n__from(X))  → ACTIVATE(X)
13:    ACTIVATE(n__s(X))  → S(activate(X))
14:    ACTIVATE(n__s(X))  → ACTIVATE(X)
The approximated dependency graph contains one SCC: {12,14}. Hence the TRS is terminating.
Tyrolean Termination Tool  (0.01 seconds)   ---  May 4, 2006